X:Type{j}, ds:x:Id fp Type{i}, da:k:Knd fp Type{i}, x:ecl(ds;da),
base:(k:Knd(State(ds)Valtype(da;k))X), seq, and, or:(ecl(ds;da)ecl(ds;da)XXX),
repeat:(ecl(ds;da)XX), act, throw:(ecl(ds;da)XX), catch:(ecl(ds;da)( List)XX).
ecl_ind(x;k,test.base(k
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq(a
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,b
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec1
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and(a
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,b
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec1
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or(a
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,b
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec1
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec2);a,rec1.repeat(a
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec2);a,rec1.repeat,rec1);a,n,rec1.act(a
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec2);a,rec1.repeat,rec1);a,n,rec1.act,n
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec2);a,rec1.repeat,rec1);a,n,rec1.act,rec1);a,n,rec1.throw(a
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec2);a,rec1.repeat,rec1);a,n,rec1.act,rec1);a,n,rec1.throw,n
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec2);a,rec1.repeat,rec1);a,n,rec1.act,rec1);a,n,rec1.throw,rec1);a,l,rec1.catch(a
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec2);a,rec1.repeat,rec1);a,n,rec1.act,rec1);a,n,rec1.throw,rec1);a,l,rec1.catch,l
ecl_ind(x;k,test.base,test);a,b,rec1,rec2.seq,rec2);a,b,rec1,rec2.and,rec2);a,b,rec1,rec2.or,rec2);a,rec1.repeat,rec1);a,n,rec1.act,rec1);a,n,rec1.throw,rec1);a,l,rec1.catch,rec1))
 X 

latex

Definitions	x. t(x), 2of(t), 1of(t), Y, x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2), ecl ind, t  T, ecl(ds;da), x:A. B(x), x(s)
Lemmas	Id wf, fpf wf, ecl wf, Knd wf, nat wf, bool wf, ma-valtype wf, decl-state wf